A famous result, conjectured by G\"odel in 1932 and proved by McKinsey andTarski in 1948, says that $\varphi$ is a theorem of intuitionisticpropositional logic IPC iff its G\"odel-translation $\varphi'$ is a theorem ofmodal logic S4. In this paper, we extend an intuitionistic version of modallogic S1+SP, introduced in our previous paper (S. Lewitzka, Algebraic semanticsfor a modal logic close to S1, J. Logic and Comp., doi:10.1093/logcom/exu067)to a classical modal logic L and prove the following: a propositional formula$\varphi$ is a theorem of IPC iff $\square\varphi$ is a theorem of L (actually,we show: $\Phi\vdash_{IPC}\varphi$ iff $\square\Phi\vdash_L\square\varphi$, forpropositional $\Phi,\varphi$). Thus, the map $\varphi\mapsto\square\varphi$ isan embedding of IPC into L, i.e. L contains a copy of IPC. Moreover, L is aconservative extension of classical propositional logic CPC. In this sense, Lis an amalgam of CPC and IPC. We show that L is sound and complete w.r.t. aclass of special Heyting algebras with a (non-normal) modal operator.
展开▼
